Left Termination of the query pattern
insert(a,a,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 581 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 501 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 PiDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 PiDP
        ↳12 PiDPToQDPProof (⇔, 0 ms)
        ↳13 QDP
        ↳14 QDPSizeChangeProof (⇔, 0 ms)
        ↳15 YES
    ↳16 PiDP
        ↳17 UsableRulesProof (⇔, 0 ms)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇒, 0 ms)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔, 0 ms)
        ↳22 YES
    ↳23 PiDP
        ↳24 UsableRulesProof (⇔, 0 ms)
        ↳25 PiDP
        ↳26 PiDPToQDPProof (⇒, 0 ms)
        ↳27 QDP
        ↳28 QDPSizeChangeProof (⇔, 0 ms)
        ↳29 YES
    ↳30 PiDP
        ↳31 UsableRulesProof (⇔, 0 ms)
        ↳32 PiDP
        ↳33 PiDPToQDPProof (⇒, 0 ms)
        ↳34 QDP
        ↳35 QDPSizeChangeProof (⇔, 0 ms)
        ↳36 YES
    ↳37 PiDP
        ↳38 UsableRulesProof (⇔, 0 ms)
        ↳39 PiDP
        ↳40 PiDPToQDPProof (⇒, 0 ms)
        ↳41 QDP
        ↳42 QDPSizeChangeProof (⇔, 0 ms)
        ↳43 YES
    ↳44 PiDP
        ↳45 UsableRulesProof (⇔, 0 ms)
        ↳46 PiDP
        ↳47 PiDPToQDPProof (⇒, 0 ms)
        ↳48 QDP
        ↳49 QDPSizeChangeProof (⇔, 0 ms)
        ↳50 YES

(0) Obligation:

Clauses:

insert(X, void, tree(X, void, void)).
insert(X, tree(X, Left, Right), tree(X, Left, Right)).
insert(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), insert(X, Left, Left1)).
insert(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), insert(X, Right, Right1)).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Query: insert(a,a,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

lessA(s(X1), s(X2)) :- lessA(X1, X2).
lessF(s(X1), s(X2)) :- lessF(X1, X2).
pD(X1, X2, X3) :- lessA(X1, X2).
pE(X1, X2, X3) :- lessF(X1, X2).
pE(X1, X2, X3) :- ','(lesscF(X1, X2), insertB(X2, X3, void)).
pJ(X1, X2, X3) :- ','(lesscL(X1), insertK(X2, X3)).
insertK(tree(X1, X2, X3), tree(X1, X4, X3)) :- pJ(X1, X2, X4).
insertK(tree(X1, X2, X3), tree(X1, X2, X4)) :- pM(X1, X3, X4).
pM(X1, X2, X3) :- ','(lesscN(X1), insertK(X2, X3)).
lessO(s(X1), s(X2)) :- lessO(X1, X2).
pP(X1, s(X2), X3, X4) :- lessO(X1, X2).
pP(X1, X2, X3, X4) :- ','(lesscR(X1, X2), insertQ(X1, X3, X4)).
insertQ(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pP(X1, X2, X3, X5).
insertQ(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pS(X2, X1, X4, X5).
pS(X1, X2, X3, X4) :- lessO(X1, s(X2)).
pS(X1, X2, X3, X4) :- ','(lesscO(X1, s(X2)), insertQ(X2, X3, X4)).
insertG(tree(X1, X2, X3), tree(X1, X4, X3)) :- pJ(X1, X2, X4).
insertG(tree(X1, X2, X3), tree(X1, X2, X4)) :- pM(X1, X3, X4).
pH(X1, X2, X3, X4) :- lessA(X1, X2).
pH(X1, X2, tree(X3, X4, X5), tree(X3, X6, X5)) :- ','(lesscA(X1, X2), pP(X1, X3, X4, X6)).
pH(X1, X2, tree(X3, X4, X5), tree(X3, X4, X6)) :- ','(lesscA(X1, X2), pS(X3, X1, X5, X6)).
pI(X1, X2, X3, X4) :- lessF(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscF(X1, X2), insertB(X2, X3, X4)).
insertB(0, tree(s(X1), X2, void), tree(s(X1), void, void)) :- insertC(X2).
insertB(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) :- pD(X1, X2, X3).
insertB(X1, tree(X2, void, X3), tree(X2, void, void)) :- pE(X2, X1, X3).
insertB(s(X1), tree(0, void, X2), tree(0, void, void)) :- insertB(s(X1), X2, void).
insertB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- lessF(X2, X1).
insertB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- ','(lesscF(X2, X1), insertB(s(X1), X3, void)).
insertB(0, tree(s(X1), X2, void), tree(s(X1), void, void)) :- insertC(X2).
insertB(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) :- pD(X1, X2, X3).
insertB(X1, tree(X2, void, X3), tree(X2, void, void)) :- pE(X2, X1, X3).
insertB(s(X1), tree(0, void, X2), tree(0, void, void)) :- insertB(s(X1), X2, void).
insertB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- lessF(X2, X1).
insertB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- ','(lesscF(X2, X1), insertB(s(X1), X3, void)).
insertB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertG(X2, X4).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pH(X1, X2, X3, X5).
insertB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pI(X2, X1, X4, X5).
insertB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertB(s(X1), X3, X4).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessF(X2, X1).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), insertB(s(X1), X4, X5)).
insertB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertG(X2, X4).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pH(X1, X2, X3, X5).
insertB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pI(X2, X1, X4, X5).
insertB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertB(s(X1), X3, X4).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessF(X2, X1).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), insertB(s(X1), X4, X5)).

Clauses:

lesscA(0, s(X1)).
lesscA(s(X1), s(X2)) :- lesscA(X1, X2).
insertcB(X1, void, tree(X1, void, void)).
insertcB(X1, tree(X1, void, void), tree(X1, void, void)).
insertcB(0, tree(s(X1), X2, void), tree(s(X1), void, void)) :- insertcC(X2).
insertcB(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) :- qcD(X1, X2, X3).
insertcB(X1, tree(X2, void, X3), tree(X2, void, void)) :- qcE(X2, X1, X3).
insertcB(s(X1), tree(0, void, X2), tree(0, void, void)) :- insertcB(s(X1), X2, void).
insertcB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- ','(lesscF(X2, X1), insertcB(s(X1), X3, void)).
insertcB(0, tree(s(X1), X2, void), tree(s(X1), void, void)) :- insertcC(X2).
insertcB(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) :- qcD(X1, X2, X3).
insertcB(X1, tree(X2, void, X3), tree(X2, void, void)) :- qcE(X2, X1, X3).
insertcB(s(X1), tree(0, void, X2), tree(0, void, void)) :- insertcB(s(X1), X2, void).
insertcB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- ','(lesscF(X2, X1), insertcB(s(X1), X3, void)).
insertcB(X1, tree(X1, X2, X3), tree(X1, X2, X3)).
insertcB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertcG(X2, X4).
insertcB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcH(X1, X2, X3, X5).
insertcB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcI(X2, X1, X4, X5).
insertcB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertcB(s(X1), X3, X4).
insertcB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), insertcB(s(X1), X4, X5)).
insertcB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertcG(X2, X4).
insertcB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcH(X1, X2, X3, X5).
insertcB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcI(X2, X1, X4, X5).
insertcB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertcB(s(X1), X3, X4).
insertcB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), insertcB(s(X1), X4, X5)).
lesscF(0, s(X1)).
lesscF(s(X1), s(X2)) :- lesscF(X1, X2).
qcE(X1, X2, X3) :- ','(lesscF(X1, X2), insertcB(X2, X3, void)).
qcJ(X1, X2, X3) :- ','(lesscL(X1), insertcK(X2, X3)).
insertcK(void, tree(0, void, void)).
insertcK(tree(0, X1, X2), tree(0, X1, X2)).
insertcK(tree(X1, X2, X3), tree(X1, X4, X3)) :- qcJ(X1, X2, X4).
insertcK(tree(X1, X2, X3), tree(X1, X2, X4)) :- qcM(X1, X3, X4).
qcM(X1, X2, X3) :- ','(lesscN(X1), insertcK(X2, X3)).
lesscO(0, s(X1)).
lesscO(s(X1), s(X2)) :- lesscO(X1, X2).
qcP(X1, X2, X3, X4) :- ','(lesscR(X1, X2), insertcQ(X1, X3, X4)).
insertcQ(X1, void, tree(s(X1), void, void)).
insertcQ(X1, tree(s(X1), X2, X3), tree(s(X1), X2, X3)).
insertcQ(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcP(X1, X2, X3, X5).
insertcQ(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcS(X2, X1, X4, X5).
qcS(X1, X2, X3, X4) :- ','(lesscO(X1, s(X2)), insertcQ(X2, X3, X4)).
insertcG(void, tree(0, void, void)).
insertcG(tree(0, X1, X2), tree(0, X1, X2)).
insertcG(tree(X1, X2, X3), tree(X1, X4, X3)) :- qcJ(X1, X2, X4).
insertcG(tree(X1, X2, X3), tree(X1, X2, X4)) :- qcM(X1, X3, X4).
qcH(X1, X2, void, tree(s(X1), void, void)) :- lesscA(X1, X2).
qcH(X1, X2, tree(s(X1), X3, X4), tree(s(X1), X3, X4)) :- lesscA(X1, X2).
qcH(X1, X2, tree(X3, X4, X5), tree(X3, X6, X5)) :- ','(lesscA(X1, X2), qcP(X1, X3, X4, X6)).
qcH(X1, X2, tree(X3, X4, X5), tree(X3, X4, X6)) :- ','(lesscA(X1, X2), qcS(X3, X1, X5, X6)).
qcI(X1, X2, X3, X4) :- ','(lesscF(X1, X2), insertcB(X2, X3, X4)).
lesscL(s(X1)).
lesscR(X1, s(X2)) :- lesscO(X1, X2).

Afs:

insertB(x1, x2, x3)  =  insertB(x3)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

lessA(s(X1), s(X2)) :- lessA(X1, X2).
lessF(s(X1), s(X2)) :- lessF(X1, X2).
pD(X1, X2, X3) :- lessA(X1, X2).
pE(X1, X2, X3) :- lessF(X1, X2).
pE(X1, X2, X3) :- ','(lesscF(X1, X2), insertB(X2, X3, void)).
pJ(X1, X2, X3) :- ','(lesscL(X1), insertK(X2, X3)).
insertK(tree(X1, X2, X3), tree(X1, X4, X3)) :- pJ(X1, X2, X4).
lessO(s(X1), s(X2)) :- lessO(X1, X2).
pP(X1, s(X2), X3, X4) :- lessO(X1, X2).
pP(X1, X2, X3, X4) :- ','(lesscR(X1, X2), insertQ(X1, X3, X4)).
insertQ(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pP(X1, X2, X3, X5).
insertQ(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pS(X2, X1, X4, X5).
pS(X1, X2, X3, X4) :- lessO(X1, s(X2)).
pS(X1, X2, X3, X4) :- ','(lesscO(X1, s(X2)), insertQ(X2, X3, X4)).
insertG(tree(X1, X2, X3), tree(X1, X4, X3)) :- pJ(X1, X2, X4).
pH(X1, X2, X3, X4) :- lessA(X1, X2).
pH(X1, X2, tree(X3, X4, X5), tree(X3, X6, X5)) :- ','(lesscA(X1, X2), pP(X1, X3, X4, X6)).
pH(X1, X2, tree(X3, X4, X5), tree(X3, X4, X6)) :- ','(lesscA(X1, X2), pS(X3, X1, X5, X6)).
pI(X1, X2, X3, X4) :- lessF(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscF(X1, X2), insertB(X2, X3, X4)).
insertB(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) :- pD(X1, X2, X3).
insertB(X1, tree(X2, void, X3), tree(X2, void, void)) :- pE(X2, X1, X3).
insertB(s(X1), tree(0, void, X2), tree(0, void, void)) :- insertB(s(X1), X2, void).
insertB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- lessF(X2, X1).
insertB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- ','(lesscF(X2, X1), insertB(s(X1), X3, void)).
insertB(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) :- pD(X1, X2, X3).
insertB(X1, tree(X2, void, X3), tree(X2, void, void)) :- pE(X2, X1, X3).
insertB(s(X1), tree(0, void, X2), tree(0, void, void)) :- insertB(s(X1), X2, void).
insertB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- lessF(X2, X1).
insertB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- ','(lesscF(X2, X1), insertB(s(X1), X3, void)).
insertB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertG(X2, X4).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pH(X1, X2, X3, X5).
insertB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pI(X2, X1, X4, X5).
insertB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertB(s(X1), X3, X4).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessF(X2, X1).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), insertB(s(X1), X4, X5)).
insertB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertG(X2, X4).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pH(X1, X2, X3, X5).
insertB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pI(X2, X1, X4, X5).
insertB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertB(s(X1), X3, X4).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessF(X2, X1).
insertB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), insertB(s(X1), X4, X5)).

Clauses:

lesscA(0, s(X1)).
lesscA(s(X1), s(X2)) :- lesscA(X1, X2).
insertcB(X1, void, tree(X1, void, void)).
insertcB(X1, tree(X1, void, void), tree(X1, void, void)).
insertcB(X1, tree(X2, void, X3), tree(X2, void, void)) :- qcE(X2, X1, X3).
insertcB(s(X1), tree(0, void, X2), tree(0, void, void)) :- insertcB(s(X1), X2, void).
insertcB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- ','(lesscF(X2, X1), insertcB(s(X1), X3, void)).
insertcB(X1, tree(X2, void, X3), tree(X2, void, void)) :- qcE(X2, X1, X3).
insertcB(s(X1), tree(0, void, X2), tree(0, void, void)) :- insertcB(s(X1), X2, void).
insertcB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) :- ','(lesscF(X2, X1), insertcB(s(X1), X3, void)).
insertcB(X1, tree(X1, X2, X3), tree(X1, X2, X3)).
insertcB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertcG(X2, X4).
insertcB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcH(X1, X2, X3, X5).
insertcB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcI(X2, X1, X4, X5).
insertcB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertcB(s(X1), X3, X4).
insertcB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), insertcB(s(X1), X4, X5)).
insertcB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- insertcG(X2, X4).
insertcB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcH(X1, X2, X3, X5).
insertcB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcI(X2, X1, X4, X5).
insertcB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- insertcB(s(X1), X3, X4).
insertcB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), insertcB(s(X1), X4, X5)).
lesscF(0, s(X1)).
lesscF(s(X1), s(X2)) :- lesscF(X1, X2).
qcE(X1, X2, X3) :- ','(lesscF(X1, X2), insertcB(X2, X3, void)).
qcJ(X1, X2, X3) :- ','(lesscL(X1), insertcK(X2, X3)).
insertcK(void, tree(0, void, void)).
insertcK(tree(0, X1, X2), tree(0, X1, X2)).
insertcK(tree(X1, X2, X3), tree(X1, X4, X3)) :- qcJ(X1, X2, X4).
lesscO(0, s(X1)).
lesscO(s(X1), s(X2)) :- lesscO(X1, X2).
qcP(X1, X2, X3, X4) :- ','(lesscR(X1, X2), insertcQ(X1, X3, X4)).
insertcQ(X1, void, tree(s(X1), void, void)).
insertcQ(X1, tree(s(X1), X2, X3), tree(s(X1), X2, X3)).
insertcQ(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcP(X1, X2, X3, X5).
insertcQ(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcS(X2, X1, X4, X5).
qcS(X1, X2, X3, X4) :- ','(lesscO(X1, s(X2)), insertcQ(X2, X3, X4)).
insertcG(void, tree(0, void, void)).
insertcG(tree(0, X1, X2), tree(0, X1, X2)).
insertcG(tree(X1, X2, X3), tree(X1, X4, X3)) :- qcJ(X1, X2, X4).
qcH(X1, X2, void, tree(s(X1), void, void)) :- lesscA(X1, X2).
qcH(X1, X2, tree(s(X1), X3, X4), tree(s(X1), X3, X4)) :- lesscA(X1, X2).
qcH(X1, X2, tree(X3, X4, X5), tree(X3, X6, X5)) :- ','(lesscA(X1, X2), qcP(X1, X3, X4, X6)).
qcH(X1, X2, tree(X3, X4, X5), tree(X3, X4, X6)) :- ','(lesscA(X1, X2), qcS(X3, X1, X5, X6)).
qcI(X1, X2, X3, X4) :- ','(lesscF(X1, X2), insertcB(X2, X3, X4)).
lesscL(s(X1)).
lesscR(X1, s(X2)) :- lesscO(X1, X2).

Afs:

insertB(x1, x2, x3)  =  insertB(x3)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
insertB_in: (f,f,b)
pD_in: (f,b,f)
lessA_in: (f,b)
pE_in: (b,f,f)
lessF_in: (b,f)
lesscF_in: (b,f)
insertG_in: (f,b)
pJ_in: (b,f,b)
insertK_in: (f,b)
pH_in: (f,b,f,b)
lesscA_in: (f,b)
pP_in: (b,b,f,b)
lessO_in: (b,b)
lesscR_in: (b,b)
lesscO_in: (b,b)
insertQ_in: (b,f,b)
pS_in: (b,b,f,b)
pI_in: (b,f,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

INSERTB_IN_AAG(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) → U28_AAG(X1, X2, X3, pD_in_aga(X1, X2, X3))
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) → PD_IN_AGA(X1, X2, X3)
PD_IN_AGA(X1, X2, X3) → U3_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
PD_IN_AGA(X1, X2, X3) → LESSA_IN_AG(X1, X2)
LESSA_IN_AG(s(X1), s(X2)) → U1_AG(X1, X2, lessA_in_ag(X1, X2))
LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)
INSERTB_IN_AAG(X1, tree(X2, void, X3), tree(X2, void, void)) → U29_AAG(X1, X2, X3, pE_in_gaa(X2, X1, X3))
INSERTB_IN_AAG(X1, tree(X2, void, X3), tree(X2, void, void)) → PE_IN_GAA(X2, X1, X3)
PE_IN_GAA(X1, X2, X3) → U4_GAA(X1, X2, X3, lessF_in_ga(X1, X2))
PE_IN_GAA(X1, X2, X3) → LESSF_IN_GA(X1, X2)
LESSF_IN_GA(s(X1), s(X2)) → U2_GA(X1, X2, lessF_in_ga(X1, X2))
LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)
PE_IN_GAA(X1, X2, X3) → U5_GAA(X1, X2, X3, lesscF_in_ga(X1, X2))
U5_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → U6_GAA(X1, X2, X3, insertB_in_aag(X2, X3, void))
U5_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → INSERTB_IN_AAG(X2, X3, void)
INSERTB_IN_AAG(s(X1), tree(0, void, X2), tree(0, void, void)) → U30_AAG(X1, X2, insertB_in_aag(s(X1), X2, void))
INSERTB_IN_AAG(s(X1), tree(0, void, X2), tree(0, void, void)) → INSERTB_IN_AAG(s(X1), X2, void)
INSERTB_IN_AAG(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) → U31_AAG(X1, X2, X3, lessF_in_ga(X2, X1))
INSERTB_IN_AAG(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) → LESSF_IN_GA(X2, X1)
INSERTB_IN_AAG(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) → U32_AAG(X1, X2, X3, lesscF_in_ga(X2, X1))
U32_AAG(X1, X2, X3, lesscF_out_ga(X2, X1)) → U33_AAG(X1, X2, X3, insertB_in_aag(s(X1), X3, void))
U32_AAG(X1, X2, X3, lesscF_out_ga(X2, X1)) → INSERTB_IN_AAG(s(X1), X3, void)
INSERTB_IN_AAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U34_AAG(X1, X2, X3, X4, insertG_in_ag(X2, X4))
INSERTB_IN_AAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTG_IN_AG(X2, X4)
INSERTG_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → U19_AG(X1, X2, X3, X4, pJ_in_gag(X1, X2, X4))
INSERTG_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → PJ_IN_GAG(X1, X2, X4)
PJ_IN_GAG(X1, X2, X3) → U7_GAG(X1, X2, X3, lesscL_in_g(X1))
U7_GAG(X1, X2, X3, lesscL_out_g(X1)) → U8_GAG(X1, X2, X3, insertK_in_ag(X2, X3))
U7_GAG(X1, X2, X3, lesscL_out_g(X1)) → INSERTK_IN_AG(X2, X3)
INSERTK_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → U9_AG(X1, X2, X3, X4, pJ_in_gag(X1, X2, X4))
INSERTK_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → PJ_IN_GAG(X1, X2, X4)
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U35_AAG(X1, X2, X3, X4, X5, pH_in_agag(X1, X2, X3, X5))
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → PH_IN_AGAG(X1, X2, X3, X5)
PH_IN_AGAG(X1, X2, X3, X4) → U20_AGAG(X1, X2, X3, X4, lessA_in_ag(X1, X2))
PH_IN_AGAG(X1, X2, X3, X4) → LESSA_IN_AG(X1, X2)
PH_IN_AGAG(X1, X2, tree(X3, X4, X5), tree(X3, X6, X5)) → U21_AGAG(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U21_AGAG(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U22_AGAG(X1, X2, X3, X4, X5, X6, pP_in_ggag(X1, X3, X4, X6))
U21_AGAG(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PP_IN_GGAG(X1, X3, X4, X6)
PP_IN_GGAG(X1, s(X2), X3, X4) → U11_GGAG(X1, X2, X3, X4, lessO_in_gg(X1, X2))
PP_IN_GGAG(X1, s(X2), X3, X4) → LESSO_IN_GG(X1, X2)
LESSO_IN_GG(s(X1), s(X2)) → U10_GG(X1, X2, lessO_in_gg(X1, X2))
LESSO_IN_GG(s(X1), s(X2)) → LESSO_IN_GG(X1, X2)
PP_IN_GGAG(X1, X2, X3, X4) → U12_GGAG(X1, X2, X3, X4, lesscR_in_gg(X1, X2))
U12_GGAG(X1, X2, X3, X4, lesscR_out_gg(X1, X2)) → U13_GGAG(X1, X2, X3, X4, insertQ_in_gag(X1, X3, X4))
U12_GGAG(X1, X2, X3, X4, lesscR_out_gg(X1, X2)) → INSERTQ_IN_GAG(X1, X3, X4)
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U14_GAG(X1, X2, X3, X4, X5, pP_in_ggag(X1, X2, X3, X5))
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PP_IN_GGAG(X1, X2, X3, X5)
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U15_GAG(X1, X2, X3, X4, X5, pS_in_ggag(X2, X1, X4, X5))
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PS_IN_GGAG(X2, X1, X4, X5)
PS_IN_GGAG(X1, X2, X3, X4) → U16_GGAG(X1, X2, X3, X4, lessO_in_gg(X1, s(X2)))
PS_IN_GGAG(X1, X2, X3, X4) → LESSO_IN_GG(X1, s(X2))
PS_IN_GGAG(X1, X2, X3, X4) → U17_GGAG(X1, X2, X3, X4, lesscO_in_gg(X1, s(X2)))
U17_GGAG(X1, X2, X3, X4, lesscO_out_gg(X1, s(X2))) → U18_GGAG(X1, X2, X3, X4, insertQ_in_gag(X2, X3, X4))
U17_GGAG(X1, X2, X3, X4, lesscO_out_gg(X1, s(X2))) → INSERTQ_IN_GAG(X2, X3, X4)
PH_IN_AGAG(X1, X2, tree(X3, X4, X5), tree(X3, X4, X6)) → U23_AGAG(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U23_AGAG(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U24_AGAG(X1, X2, X3, X4, X5, X6, pS_in_ggag(X3, X1, X5, X6))
U23_AGAG(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PS_IN_GGAG(X3, X1, X5, X6)
INSERTB_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U36_AAG(X1, X2, X3, X4, X5, pI_in_gaag(X2, X1, X4, X5))
INSERTB_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PI_IN_GAAG(X2, X1, X4, X5)
PI_IN_GAAG(X1, X2, X3, X4) → U25_GAAG(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PI_IN_GAAG(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PI_IN_GAAG(X1, X2, X3, X4) → U26_GAAG(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U26_GAAG(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U27_GAAG(X1, X2, X3, X4, insertB_in_aag(X2, X3, X4))
U26_GAAG(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → INSERTB_IN_AAG(X2, X3, X4)
INSERTB_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U37_AAG(X1, X2, X3, X4, insertB_in_aag(s(X1), X3, X4))
INSERTB_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTB_IN_AAG(s(X1), X3, X4)
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U38_AAG(X1, X2, X3, X4, X5, lessF_in_ga(X2, X1))
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSF_IN_GA(X2, X1)
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U39_AAG(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U39_AAG(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → U40_AAG(X1, X2, X3, X4, X5, insertB_in_aag(s(X1), X4, X5))
U39_AAG(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → INSERTB_IN_AAG(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U42_ag(X1, X2, lesscA_in_ag(X1, X2))
U42_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))

The argument filtering Pi contains the following mapping:
insertB_in_aag(x1, x2, x3)  =  insertB_in_aag(x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
void  =  void
pD_in_aga(x1, x2, x3)  =  pD_in_aga(x2)
lessA_in_ag(x1, x2)  =  lessA_in_ag(x2)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
lessF_in_ga(x1, x2)  =  lessF_in_ga(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
insertG_in_ag(x1, x2)  =  insertG_in_ag(x2)
pJ_in_gag(x1, x2, x3)  =  pJ_in_gag(x1, x3)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
insertK_in_ag(x1, x2)  =  insertK_in_ag(x2)
pH_in_agag(x1, x2, x3, x4)  =  pH_in_agag(x2, x4)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U42_ag(x1, x2, x3)  =  U42_ag(x2, x3)
pP_in_ggag(x1, x2, x3, x4)  =  pP_in_ggag(x1, x2, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
insertQ_in_gag(x1, x2, x3)  =  insertQ_in_gag(x1, x3)
pS_in_ggag(x1, x2, x3, x4)  =  pS_in_ggag(x1, x2, x4)
pI_in_gaag(x1, x2, x3, x4)  =  pI_in_gaag(x1, x4)
INSERTB_IN_AAG(x1, x2, x3)  =  INSERTB_IN_AAG(x3)
U28_AAG(x1, x2, x3, x4)  =  U28_AAG(x2, x4)
PD_IN_AGA(x1, x2, x3)  =  PD_IN_AGA(x2)
U3_AGA(x1, x2, x3, x4)  =  U3_AGA(x2, x4)
LESSA_IN_AG(x1, x2)  =  LESSA_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
U29_AAG(x1, x2, x3, x4)  =  U29_AAG(x2, x4)
PE_IN_GAA(x1, x2, x3)  =  PE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
LESSF_IN_GA(x1, x2)  =  LESSF_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
U30_AAG(x1, x2, x3)  =  U30_AAG(x3)
U31_AAG(x1, x2, x3, x4)  =  U31_AAG(x2, x4)
U32_AAG(x1, x2, x3, x4)  =  U32_AAG(x2, x4)
U33_AAG(x1, x2, x3, x4)  =  U33_AAG(x2, x4)
U34_AAG(x1, x2, x3, x4, x5)  =  U34_AAG(x1, x3, x4, x5)
INSERTG_IN_AG(x1, x2)  =  INSERTG_IN_AG(x2)
U19_AG(x1, x2, x3, x4, x5)  =  U19_AG(x1, x3, x4, x5)
PJ_IN_GAG(x1, x2, x3)  =  PJ_IN_GAG(x1, x3)
U7_GAG(x1, x2, x3, x4)  =  U7_GAG(x1, x3, x4)
U8_GAG(x1, x2, x3, x4)  =  U8_GAG(x1, x3, x4)
INSERTK_IN_AG(x1, x2)  =  INSERTK_IN_AG(x2)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x1, x3, x4, x5)
U35_AAG(x1, x2, x3, x4, x5, x6)  =  U35_AAG(x2, x4, x5, x6)
PH_IN_AGAG(x1, x2, x3, x4)  =  PH_IN_AGAG(x2, x4)
U20_AGAG(x1, x2, x3, x4, x5)  =  U20_AGAG(x2, x4, x5)
U21_AGAG(x1, x2, x3, x4, x5, x6, x7)  =  U21_AGAG(x2, x3, x5, x6, x7)
U22_AGAG(x1, x2, x3, x4, x5, x6, x7)  =  U22_AGAG(x1, x2, x3, x5, x6, x7)
PP_IN_GGAG(x1, x2, x3, x4)  =  PP_IN_GGAG(x1, x2, x4)
U11_GGAG(x1, x2, x3, x4, x5)  =  U11_GGAG(x1, x2, x4, x5)
LESSO_IN_GG(x1, x2)  =  LESSO_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x1, x2, x3)
U12_GGAG(x1, x2, x3, x4, x5)  =  U12_GGAG(x1, x2, x4, x5)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)
INSERTQ_IN_GAG(x1, x2, x3)  =  INSERTQ_IN_GAG(x1, x3)
U14_GAG(x1, x2, x3, x4, x5, x6)  =  U14_GAG(x1, x2, x4, x5, x6)
U15_GAG(x1, x2, x3, x4, x5, x6)  =  U15_GAG(x1, x2, x3, x5, x6)
PS_IN_GGAG(x1, x2, x3, x4)  =  PS_IN_GGAG(x1, x2, x4)
U16_GGAG(x1, x2, x3, x4, x5)  =  U16_GGAG(x1, x2, x4, x5)
U17_GGAG(x1, x2, x3, x4, x5)  =  U17_GGAG(x1, x2, x4, x5)
U18_GGAG(x1, x2, x3, x4, x5)  =  U18_GGAG(x1, x2, x4, x5)
U23_AGAG(x1, x2, x3, x4, x5, x6, x7)  =  U23_AGAG(x2, x3, x4, x6, x7)
U24_AGAG(x1, x2, x3, x4, x5, x6, x7)  =  U24_AGAG(x1, x2, x3, x4, x6, x7)
U36_AAG(x1, x2, x3, x4, x5, x6)  =  U36_AAG(x2, x3, x5, x6)
PI_IN_GAAG(x1, x2, x3, x4)  =  PI_IN_GAAG(x1, x4)
U25_GAAG(x1, x2, x3, x4, x5)  =  U25_GAAG(x1, x4, x5)
U26_GAAG(x1, x2, x3, x4, x5)  =  U26_GAAG(x1, x4, x5)
U27_GAAG(x1, x2, x3, x4, x5)  =  U27_GAAG(x1, x4, x5)
U37_AAG(x1, x2, x3, x4, x5)  =  U37_AAG(x2, x4, x5)
U38_AAG(x1, x2, x3, x4, x5, x6)  =  U38_AAG(x2, x3, x5, x6)
U39_AAG(x1, x2, x3, x4, x5, x6)  =  U39_AAG(x2, x3, x5, x6)
U40_AAG(x1, x2, x3, x4, x5, x6)  =  U40_AAG(x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INSERTB_IN_AAG(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) → U28_AAG(X1, X2, X3, pD_in_aga(X1, X2, X3))
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, void), tree(s(X2), void, void)) → PD_IN_AGA(X1, X2, X3)
PD_IN_AGA(X1, X2, X3) → U3_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
PD_IN_AGA(X1, X2, X3) → LESSA_IN_AG(X1, X2)
LESSA_IN_AG(s(X1), s(X2)) → U1_AG(X1, X2, lessA_in_ag(X1, X2))
LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)
INSERTB_IN_AAG(X1, tree(X2, void, X3), tree(X2, void, void)) → U29_AAG(X1, X2, X3, pE_in_gaa(X2, X1, X3))
INSERTB_IN_AAG(X1, tree(X2, void, X3), tree(X2, void, void)) → PE_IN_GAA(X2, X1, X3)
PE_IN_GAA(X1, X2, X3) → U4_GAA(X1, X2, X3, lessF_in_ga(X1, X2))
PE_IN_GAA(X1, X2, X3) → LESSF_IN_GA(X1, X2)
LESSF_IN_GA(s(X1), s(X2)) → U2_GA(X1, X2, lessF_in_ga(X1, X2))
LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)
PE_IN_GAA(X1, X2, X3) → U5_GAA(X1, X2, X3, lesscF_in_ga(X1, X2))
U5_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → U6_GAA(X1, X2, X3, insertB_in_aag(X2, X3, void))
U5_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → INSERTB_IN_AAG(X2, X3, void)
INSERTB_IN_AAG(s(X1), tree(0, void, X2), tree(0, void, void)) → U30_AAG(X1, X2, insertB_in_aag(s(X1), X2, void))
INSERTB_IN_AAG(s(X1), tree(0, void, X2), tree(0, void, void)) → INSERTB_IN_AAG(s(X1), X2, void)
INSERTB_IN_AAG(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) → U31_AAG(X1, X2, X3, lessF_in_ga(X2, X1))
INSERTB_IN_AAG(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) → LESSF_IN_GA(X2, X1)
INSERTB_IN_AAG(s(X1), tree(s(X2), void, X3), tree(s(X2), void, void)) → U32_AAG(X1, X2, X3, lesscF_in_ga(X2, X1))
U32_AAG(X1, X2, X3, lesscF_out_ga(X2, X1)) → U33_AAG(X1, X2, X3, insertB_in_aag(s(X1), X3, void))
U32_AAG(X1, X2, X3, lesscF_out_ga(X2, X1)) → INSERTB_IN_AAG(s(X1), X3, void)
INSERTB_IN_AAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U34_AAG(X1, X2, X3, X4, insertG_in_ag(X2, X4))
INSERTB_IN_AAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → INSERTG_IN_AG(X2, X4)
INSERTG_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → U19_AG(X1, X2, X3, X4, pJ_in_gag(X1, X2, X4))
INSERTG_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → PJ_IN_GAG(X1, X2, X4)
PJ_IN_GAG(X1, X2, X3) → U7_GAG(X1, X2, X3, lesscL_in_g(X1))
U7_GAG(X1, X2, X3, lesscL_out_g(X1)) → U8_GAG(X1, X2, X3, insertK_in_ag(X2, X3))
U7_GAG(X1, X2, X3, lesscL_out_g(X1)) → INSERTK_IN_AG(X2, X3)
INSERTK_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → U9_AG(X1, X2, X3, X4, pJ_in_gag(X1, X2, X4))
INSERTK_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → PJ_IN_GAG(X1, X2, X4)
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U35_AAG(X1, X2, X3, X4, X5, pH_in_agag(X1, X2, X3, X5))
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → PH_IN_AGAG(X1, X2, X3, X5)
PH_IN_AGAG(X1, X2, X3, X4) → U20_AGAG(X1, X2, X3, X4, lessA_in_ag(X1, X2))
PH_IN_AGAG(X1, X2, X3, X4) → LESSA_IN_AG(X1, X2)
PH_IN_AGAG(X1, X2, tree(X3, X4, X5), tree(X3, X6, X5)) → U21_AGAG(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U21_AGAG(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U22_AGAG(X1, X2, X3, X4, X5, X6, pP_in_ggag(X1, X3, X4, X6))
U21_AGAG(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PP_IN_GGAG(X1, X3, X4, X6)
PP_IN_GGAG(X1, s(X2), X3, X4) → U11_GGAG(X1, X2, X3, X4, lessO_in_gg(X1, X2))
PP_IN_GGAG(X1, s(X2), X3, X4) → LESSO_IN_GG(X1, X2)
LESSO_IN_GG(s(X1), s(X2)) → U10_GG(X1, X2, lessO_in_gg(X1, X2))
LESSO_IN_GG(s(X1), s(X2)) → LESSO_IN_GG(X1, X2)
PP_IN_GGAG(X1, X2, X3, X4) → U12_GGAG(X1, X2, X3, X4, lesscR_in_gg(X1, X2))
U12_GGAG(X1, X2, X3, X4, lesscR_out_gg(X1, X2)) → U13_GGAG(X1, X2, X3, X4, insertQ_in_gag(X1, X3, X4))
U12_GGAG(X1, X2, X3, X4, lesscR_out_gg(X1, X2)) → INSERTQ_IN_GAG(X1, X3, X4)
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U14_GAG(X1, X2, X3, X4, X5, pP_in_ggag(X1, X2, X3, X5))
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PP_IN_GGAG(X1, X2, X3, X5)
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U15_GAG(X1, X2, X3, X4, X5, pS_in_ggag(X2, X1, X4, X5))
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PS_IN_GGAG(X2, X1, X4, X5)
PS_IN_GGAG(X1, X2, X3, X4) → U16_GGAG(X1, X2, X3, X4, lessO_in_gg(X1, s(X2)))
PS_IN_GGAG(X1, X2, X3, X4) → LESSO_IN_GG(X1, s(X2))
PS_IN_GGAG(X1, X2, X3, X4) → U17_GGAG(X1, X2, X3, X4, lesscO_in_gg(X1, s(X2)))
U17_GGAG(X1, X2, X3, X4, lesscO_out_gg(X1, s(X2))) → U18_GGAG(X1, X2, X3, X4, insertQ_in_gag(X2, X3, X4))
U17_GGAG(X1, X2, X3, X4, lesscO_out_gg(X1, s(X2))) → INSERTQ_IN_GAG(X2, X3, X4)
PH_IN_AGAG(X1, X2, tree(X3, X4, X5), tree(X3, X4, X6)) → U23_AGAG(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U23_AGAG(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U24_AGAG(X1, X2, X3, X4, X5, X6, pS_in_ggag(X3, X1, X5, X6))
U23_AGAG(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PS_IN_GGAG(X3, X1, X5, X6)
INSERTB_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U36_AAG(X1, X2, X3, X4, X5, pI_in_gaag(X2, X1, X4, X5))
INSERTB_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PI_IN_GAAG(X2, X1, X4, X5)
PI_IN_GAAG(X1, X2, X3, X4) → U25_GAAG(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PI_IN_GAAG(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PI_IN_GAAG(X1, X2, X3, X4) → U26_GAAG(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U26_GAAG(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U27_GAAG(X1, X2, X3, X4, insertB_in_aag(X2, X3, X4))
U26_GAAG(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → INSERTB_IN_AAG(X2, X3, X4)
INSERTB_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U37_AAG(X1, X2, X3, X4, insertB_in_aag(s(X1), X3, X4))
INSERTB_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTB_IN_AAG(s(X1), X3, X4)
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U38_AAG(X1, X2, X3, X4, X5, lessF_in_ga(X2, X1))
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSF_IN_GA(X2, X1)
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U39_AAG(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U39_AAG(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → U40_AAG(X1, X2, X3, X4, X5, insertB_in_aag(s(X1), X4, X5))
U39_AAG(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → INSERTB_IN_AAG(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U42_ag(X1, X2, lesscA_in_ag(X1, X2))
U42_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))

The argument filtering Pi contains the following mapping:
insertB_in_aag(x1, x2, x3)  =  insertB_in_aag(x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
void  =  void
pD_in_aga(x1, x2, x3)  =  pD_in_aga(x2)
lessA_in_ag(x1, x2)  =  lessA_in_ag(x2)
pE_in_gaa(x1, x2, x3)  =  pE_in_gaa(x1)
lessF_in_ga(x1, x2)  =  lessF_in_ga(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
insertG_in_ag(x1, x2)  =  insertG_in_ag(x2)
pJ_in_gag(x1, x2, x3)  =  pJ_in_gag(x1, x3)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
insertK_in_ag(x1, x2)  =  insertK_in_ag(x2)
pH_in_agag(x1, x2, x3, x4)  =  pH_in_agag(x2, x4)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U42_ag(x1, x2, x3)  =  U42_ag(x2, x3)
pP_in_ggag(x1, x2, x3, x4)  =  pP_in_ggag(x1, x2, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
insertQ_in_gag(x1, x2, x3)  =  insertQ_in_gag(x1, x3)
pS_in_ggag(x1, x2, x3, x4)  =  pS_in_ggag(x1, x2, x4)
pI_in_gaag(x1, x2, x3, x4)  =  pI_in_gaag(x1, x4)
INSERTB_IN_AAG(x1, x2, x3)  =  INSERTB_IN_AAG(x3)
U28_AAG(x1, x2, x3, x4)  =  U28_AAG(x2, x4)
PD_IN_AGA(x1, x2, x3)  =  PD_IN_AGA(x2)
U3_AGA(x1, x2, x3, x4)  =  U3_AGA(x2, x4)
LESSA_IN_AG(x1, x2)  =  LESSA_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
U29_AAG(x1, x2, x3, x4)  =  U29_AAG(x2, x4)
PE_IN_GAA(x1, x2, x3)  =  PE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
LESSF_IN_GA(x1, x2)  =  LESSF_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
U30_AAG(x1, x2, x3)  =  U30_AAG(x3)
U31_AAG(x1, x2, x3, x4)  =  U31_AAG(x2, x4)
U32_AAG(x1, x2, x3, x4)  =  U32_AAG(x2, x4)
U33_AAG(x1, x2, x3, x4)  =  U33_AAG(x2, x4)
U34_AAG(x1, x2, x3, x4, x5)  =  U34_AAG(x1, x3, x4, x5)
INSERTG_IN_AG(x1, x2)  =  INSERTG_IN_AG(x2)
U19_AG(x1, x2, x3, x4, x5)  =  U19_AG(x1, x3, x4, x5)
PJ_IN_GAG(x1, x2, x3)  =  PJ_IN_GAG(x1, x3)
U7_GAG(x1, x2, x3, x4)  =  U7_GAG(x1, x3, x4)
U8_GAG(x1, x2, x3, x4)  =  U8_GAG(x1, x3, x4)
INSERTK_IN_AG(x1, x2)  =  INSERTK_IN_AG(x2)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x1, x3, x4, x5)
U35_AAG(x1, x2, x3, x4, x5, x6)  =  U35_AAG(x2, x4, x5, x6)
PH_IN_AGAG(x1, x2, x3, x4)  =  PH_IN_AGAG(x2, x4)
U20_AGAG(x1, x2, x3, x4, x5)  =  U20_AGAG(x2, x4, x5)
U21_AGAG(x1, x2, x3, x4, x5, x6, x7)  =  U21_AGAG(x2, x3, x5, x6, x7)
U22_AGAG(x1, x2, x3, x4, x5, x6, x7)  =  U22_AGAG(x1, x2, x3, x5, x6, x7)
PP_IN_GGAG(x1, x2, x3, x4)  =  PP_IN_GGAG(x1, x2, x4)
U11_GGAG(x1, x2, x3, x4, x5)  =  U11_GGAG(x1, x2, x4, x5)
LESSO_IN_GG(x1, x2)  =  LESSO_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x1, x2, x3)
U12_GGAG(x1, x2, x3, x4, x5)  =  U12_GGAG(x1, x2, x4, x5)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)
INSERTQ_IN_GAG(x1, x2, x3)  =  INSERTQ_IN_GAG(x1, x3)
U14_GAG(x1, x2, x3, x4, x5, x6)  =  U14_GAG(x1, x2, x4, x5, x6)
U15_GAG(x1, x2, x3, x4, x5, x6)  =  U15_GAG(x1, x2, x3, x5, x6)
PS_IN_GGAG(x1, x2, x3, x4)  =  PS_IN_GGAG(x1, x2, x4)
U16_GGAG(x1, x2, x3, x4, x5)  =  U16_GGAG(x1, x2, x4, x5)
U17_GGAG(x1, x2, x3, x4, x5)  =  U17_GGAG(x1, x2, x4, x5)
U18_GGAG(x1, x2, x3, x4, x5)  =  U18_GGAG(x1, x2, x4, x5)
U23_AGAG(x1, x2, x3, x4, x5, x6, x7)  =  U23_AGAG(x2, x3, x4, x6, x7)
U24_AGAG(x1, x2, x3, x4, x5, x6, x7)  =  U24_AGAG(x1, x2, x3, x4, x6, x7)
U36_AAG(x1, x2, x3, x4, x5, x6)  =  U36_AAG(x2, x3, x5, x6)
PI_IN_GAAG(x1, x2, x3, x4)  =  PI_IN_GAAG(x1, x4)
U25_GAAG(x1, x2, x3, x4, x5)  =  U25_GAAG(x1, x4, x5)
U26_GAAG(x1, x2, x3, x4, x5)  =  U26_GAAG(x1, x4, x5)
U27_GAAG(x1, x2, x3, x4, x5)  =  U27_GAAG(x1, x4, x5)
U37_AAG(x1, x2, x3, x4, x5)  =  U37_AAG(x2, x4, x5)
U38_AAG(x1, x2, x3, x4, x5, x6)  =  U38_AAG(x2, x3, x5, x6)
U39_AAG(x1, x2, x3, x4, x5, x6)  =  U39_AAG(x2, x3, x5, x6)
U40_AAG(x1, x2, x3, x4, x5, x6)  =  U40_AAG(x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 53 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSO_IN_GG(s(X1), s(X2)) → LESSO_IN_GG(X1, X2)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U42_ag(X1, X2, lesscA_in_ag(X1, X2))
U42_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U42_ag(x1, x2, x3)  =  U42_ag(x2, x3)
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
LESSO_IN_GG(x1, x2)  =  LESSO_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSO_IN_GG(s(X1), s(X2)) → LESSO_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSO_IN_GG(s(X1), s(X2)) → LESSO_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSO_IN_GG(s(X1), s(X2)) → LESSO_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PP_IN_GGAG(X1, X2, X3, X4) → U12_GGAG(X1, X2, X3, X4, lesscR_in_gg(X1, X2))
U12_GGAG(X1, X2, X3, X4, lesscR_out_gg(X1, X2)) → INSERTQ_IN_GAG(X1, X3, X4)
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PP_IN_GGAG(X1, X2, X3, X5)
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PS_IN_GGAG(X2, X1, X4, X5)
PS_IN_GGAG(X1, X2, X3, X4) → U17_GGAG(X1, X2, X3, X4, lesscO_in_gg(X1, s(X2)))
U17_GGAG(X1, X2, X3, X4, lesscO_out_gg(X1, s(X2))) → INSERTQ_IN_GAG(X2, X3, X4)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U42_ag(X1, X2, lesscA_in_ag(X1, X2))
U42_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U42_ag(x1, x2, x3)  =  U42_ag(x2, x3)
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
PP_IN_GGAG(x1, x2, x3, x4)  =  PP_IN_GGAG(x1, x2, x4)
U12_GGAG(x1, x2, x3, x4, x5)  =  U12_GGAG(x1, x2, x4, x5)
INSERTQ_IN_GAG(x1, x2, x3)  =  INSERTQ_IN_GAG(x1, x3)
PS_IN_GGAG(x1, x2, x3, x4)  =  PS_IN_GGAG(x1, x2, x4)
U17_GGAG(x1, x2, x3, x4, x5)  =  U17_GGAG(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PP_IN_GGAG(X1, X2, X3, X4) → U12_GGAG(X1, X2, X3, X4, lesscR_in_gg(X1, X2))
U12_GGAG(X1, X2, X3, X4, lesscR_out_gg(X1, X2)) → INSERTQ_IN_GAG(X1, X3, X4)
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PP_IN_GGAG(X1, X2, X3, X5)
INSERTQ_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PS_IN_GGAG(X2, X1, X4, X5)
PS_IN_GGAG(X1, X2, X3, X4) → U17_GGAG(X1, X2, X3, X4, lesscO_in_gg(X1, s(X2)))
U17_GGAG(X1, X2, X3, X4, lesscO_out_gg(X1, s(X2))) → INSERTQ_IN_GAG(X2, X3, X4)

The TRS R consists of the following rules:

lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
0  =  0
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
PP_IN_GGAG(x1, x2, x3, x4)  =  PP_IN_GGAG(x1, x2, x4)
U12_GGAG(x1, x2, x3, x4, x5)  =  U12_GGAG(x1, x2, x4, x5)
INSERTQ_IN_GAG(x1, x2, x3)  =  INSERTQ_IN_GAG(x1, x3)
PS_IN_GGAG(x1, x2, x3, x4)  =  PS_IN_GGAG(x1, x2, x4)
U17_GGAG(x1, x2, x3, x4, x5)  =  U17_GGAG(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PP_IN_GGAG(X1, X2, X4) → U12_GGAG(X1, X2, X4, lesscR_in_gg(X1, X2))
U12_GGAG(X1, X2, X4, lesscR_out_gg(X1, X2)) → INSERTQ_IN_GAG(X1, X4)
INSERTQ_IN_GAG(X1, tree(X2, X5, X4)) → PP_IN_GGAG(X1, X2, X5)
INSERTQ_IN_GAG(X1, tree(X2, X3, X5)) → PS_IN_GGAG(X2, X1, X5)
PS_IN_GGAG(X1, X2, X4) → U17_GGAG(X1, X2, X4, lesscO_in_gg(X1, s(X2)))
U17_GGAG(X1, X2, X4, lesscO_out_gg(X1, s(X2))) → INSERTQ_IN_GAG(X2, X4)

The TRS R consists of the following rules:

lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lesscR_in_gg(x0, x1)
lesscO_in_gg(x0, x1)
U75_gg(x0, x1, x2)
U59_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U12_GGAG(X1, X2, X4, lesscR_out_gg(X1, X2)) → INSERTQ_IN_GAG(X1, X4)
    The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

  • INSERTQ_IN_GAG(X1, tree(X2, X5, X4)) → PP_IN_GGAG(X1, X2, X5)
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • INSERTQ_IN_GAG(X1, tree(X2, X3, X5)) → PS_IN_GGAG(X2, X1, X5)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • PP_IN_GGAG(X1, X2, X4) → U12_GGAG(X1, X2, X4, lesscR_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U17_GGAG(X1, X2, X4, lesscO_out_gg(X1, s(X2))) → INSERTQ_IN_GAG(X2, X4)
    The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

  • PS_IN_GGAG(X1, X2, X4) → U17_GGAG(X1, X2, X4, lesscO_in_gg(X1, s(X2)))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U7_GAG(X1, X2, X3, lesscL_out_g(X1)) → INSERTK_IN_AG(X2, X3)
INSERTK_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → PJ_IN_GAG(X1, X2, X4)
PJ_IN_GAG(X1, X2, X3) → U7_GAG(X1, X2, X3, lesscL_in_g(X1))

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U42_ag(X1, X2, lesscA_in_ag(X1, X2))
U42_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U42_ag(x1, x2, x3)  =  U42_ag(x2, x3)
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
PJ_IN_GAG(x1, x2, x3)  =  PJ_IN_GAG(x1, x3)
U7_GAG(x1, x2, x3, x4)  =  U7_GAG(x1, x3, x4)
INSERTK_IN_AG(x1, x2)  =  INSERTK_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U7_GAG(X1, X2, X3, lesscL_out_g(X1)) → INSERTK_IN_AG(X2, X3)
INSERTK_IN_AG(tree(X1, X2, X3), tree(X1, X4, X3)) → PJ_IN_GAG(X1, X2, X4)
PJ_IN_GAG(X1, X2, X3) → U7_GAG(X1, X2, X3, lesscL_in_g(X1))

The TRS R consists of the following rules:

lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
PJ_IN_GAG(x1, x2, x3)  =  PJ_IN_GAG(x1, x3)
U7_GAG(x1, x2, x3, x4)  =  U7_GAG(x1, x3, x4)
INSERTK_IN_AG(x1, x2)  =  INSERTK_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U7_GAG(X1, X3, lesscL_out_g(X1)) → INSERTK_IN_AG(X3)
INSERTK_IN_AG(tree(X1, X4, X3)) → PJ_IN_GAG(X1, X4)
PJ_IN_GAG(X1, X3) → U7_GAG(X1, X3, lesscL_in_g(X1))

The TRS R consists of the following rules:

lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))

The set Q consists of the following terms:

lesscL_in_g(x0)

We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • INSERTK_IN_AG(tree(X1, X4, X3)) → PJ_IN_GAG(X1, X4)
    The graph contains the following edges 1 > 1, 1 > 2

  • PJ_IN_GAG(X1, X3) → U7_GAG(X1, X3, lesscL_in_g(X1))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U7_GAG(X1, X3, lesscL_out_g(X1)) → INSERTK_IN_AG(X3)
    The graph contains the following edges 2 >= 1

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U42_ag(X1, X2, lesscA_in_ag(X1, X2))
U42_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U42_ag(x1, x2, x3)  =  U42_ag(x2, x3)
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
LESSF_IN_GA(x1, x2)  =  LESSF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSF_IN_GA(x1, x2)  =  LESSF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSF_IN_GA(s(X1)) → LESSF_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSF_IN_GA(s(X1)) → LESSF_IN_GA(X1)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U42_ag(X1, X2, lesscA_in_ag(X1, X2))
U42_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U42_ag(x1, x2, x3)  =  U42_ag(x2, x3)
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
LESSA_IN_AG(x1, x2)  =  LESSA_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSA_IN_AG(x1, x2)  =  LESSA_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSA_IN_AG(s(X2)) → LESSA_IN_AG(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSA_IN_AG(s(X2)) → LESSA_IN_AG(X2)
    The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INSERTB_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PI_IN_GAAG(X2, X1, X4, X5)
PI_IN_GAAG(X1, X2, X3, X4) → U26_GAAG(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U26_GAAG(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → INSERTB_IN_AAG(X2, X3, X4)
INSERTB_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTB_IN_AAG(s(X1), X3, X4)
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U39_AAG(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U39_AAG(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → INSERTB_IN_AAG(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscL_in_g(s(X1)) → lesscL_out_g(s(X1))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U42_ag(X1, X2, lesscA_in_ag(X1, X2))
U42_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscR_in_gg(X1, s(X2)) → U75_gg(X1, X2, lesscO_in_gg(X1, X2))
lesscO_in_gg(0, s(X1)) → lesscO_out_gg(0, s(X1))
lesscO_in_gg(s(X1), s(X2)) → U59_gg(X1, X2, lesscO_in_gg(X1, X2))
U59_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscO_out_gg(s(X1), s(X2))
U75_gg(X1, X2, lesscO_out_gg(X1, X2)) → lesscR_out_gg(X1, s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
lesscL_in_g(x1)  =  lesscL_in_g(x1)
lesscL_out_g(x1)  =  lesscL_out_g(x1)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U42_ag(x1, x2, x3)  =  U42_ag(x2, x3)
lesscR_in_gg(x1, x2)  =  lesscR_in_gg(x1, x2)
U75_gg(x1, x2, x3)  =  U75_gg(x1, x2, x3)
lesscO_in_gg(x1, x2)  =  lesscO_in_gg(x1, x2)
lesscO_out_gg(x1, x2)  =  lesscO_out_gg(x1, x2)
U59_gg(x1, x2, x3)  =  U59_gg(x1, x2, x3)
lesscR_out_gg(x1, x2)  =  lesscR_out_gg(x1, x2)
INSERTB_IN_AAG(x1, x2, x3)  =  INSERTB_IN_AAG(x3)
PI_IN_GAAG(x1, x2, x3, x4)  =  PI_IN_GAAG(x1, x4)
U26_GAAG(x1, x2, x3, x4, x5)  =  U26_GAAG(x1, x4, x5)
U39_AAG(x1, x2, x3, x4, x5, x6)  =  U39_AAG(x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INSERTB_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PI_IN_GAAG(X2, X1, X4, X5)
PI_IN_GAAG(X1, X2, X3, X4) → U26_GAAG(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U26_GAAG(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → INSERTB_IN_AAG(X2, X3, X4)
INSERTB_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → INSERTB_IN_AAG(s(X1), X3, X4)
INSERTB_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U39_AAG(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U39_AAG(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → INSERTB_IN_AAG(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U53_ga(X1, X2, lesscF_in_ga(X1, X2))
U53_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
INSERTB_IN_AAG(x1, x2, x3)  =  INSERTB_IN_AAG(x3)
PI_IN_GAAG(x1, x2, x3, x4)  =  PI_IN_GAAG(x1, x4)
U26_GAAG(x1, x2, x3, x4, x5)  =  U26_GAAG(x1, x4, x5)
U39_AAG(x1, x2, x3, x4, x5, x6)  =  U39_AAG(x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INSERTB_IN_AAG(tree(X2, X3, X5)) → PI_IN_GAAG(X2, X5)
PI_IN_GAAG(X1, X4) → U26_GAAG(X1, X4, lesscF_in_ga(X1))
U26_GAAG(X1, X4, lesscF_out_ga(X1)) → INSERTB_IN_AAG(X4)
INSERTB_IN_AAG(tree(0, X2, X4)) → INSERTB_IN_AAG(X4)
INSERTB_IN_AAG(tree(s(X2), X3, X5)) → U39_AAG(X2, X3, X5, lesscF_in_ga(X2))
U39_AAG(X2, X3, X5, lesscF_out_ga(X2)) → INSERTB_IN_AAG(X5)

The TRS R consists of the following rules:

lesscF_in_ga(0) → lesscF_out_ga(0)
lesscF_in_ga(s(X1)) → U53_ga(X1, lesscF_in_ga(X1))
U53_ga(X1, lesscF_out_ga(X1)) → lesscF_out_ga(s(X1))

The set Q consists of the following terms:

lesscF_in_ga(x0)
U53_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PI_IN_GAAG(X1, X4) → U26_GAAG(X1, X4, lesscF_in_ga(X1))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U26_GAAG(X1, X4, lesscF_out_ga(X1)) → INSERTB_IN_AAG(X4)
    The graph contains the following edges 2 >= 1

  • INSERTB_IN_AAG(tree(X2, X3, X5)) → PI_IN_GAAG(X2, X5)
    The graph contains the following edges 1 > 1, 1 > 2

  • INSERTB_IN_AAG(tree(s(X2), X3, X5)) → U39_AAG(X2, X3, X5, lesscF_in_ga(X2))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

  • INSERTB_IN_AAG(tree(0, X2, X4)) → INSERTB_IN_AAG(X4)
    The graph contains the following edges 1 > 1

  • U39_AAG(X2, X3, X5, lesscF_out_ga(X2)) → INSERTB_IN_AAG(X5)
    The graph contains the following edges 3 >= 1

(50) YES